\begin{tabbing}
ES(${\it the\_w}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$E\+
\\[0ex], product{-}deq(Id;$\mathbb{N}$;IdDeq;NatDeq)
\\[0ex], $\lambda$$e$.w{-}pred(${\it the\_w}$;$e$)
\\[0ex], $\lambda$$e$.w{-}info(${\it the\_w}$;$e$)
\\[0ex], TERMOF\{w{-}order{-}axioms:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], ${\it the\_w}$.T
\\[0ex], ${\it the\_w}$.TA
\\[0ex], ${\it the\_w}$.M
\\[0ex], $\lambda$$i$,$x$. s($i$;0).$x$
\\[0ex], $\lambda$$i$.(w{-}machine(${\it the\_w}$;$i$).2).1
\\[0ex], $\lambda$$e$.val($e$)
\\[0ex], $\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).2.2
\\[0ex], $\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).1
\\[0ex], $\lambda$$e$.time($e$)
\\[0ex], TERMOF\{world{-}es{-}val:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], TERMOF\{w{-}causl{-}time2:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], $\lambda$$i$,$x$. discrete($i$;$x$)
\\[0ex], TERMOF\{world{-}es{-}const:ObjectId, 1:l, i:l\}(${\it the\_w}$,$p$)
\\[0ex], $\cdot>$
\-
\end{tabbing}